| Definitions | t  T, Id, P   Q,  x:A. B(x), sender(e), s = t, rcv?(e),  b, Type, prop{i:l}, A c B, x:A  B(x), P  Q, pred!(e;e'), pred(e), first(e),  A, a < b, x:A  B(x),  , {x:A| B(x)} ,  x:A. B(x), SWellFounded(R(x;y)), IdLnk, <a, b>, True,  T, Msg(M), haslink(l; m), type List, P Q, tag(k), lnk(k), act(k), islocal(k), Msg_sub(l; M), rcv(l,tg), void, False, Knd,   x,y. t(x;y), x. t(x), EOrderAxioms(E;pred?;info), sends(dE; dL; pred?; info; val; p; e; l), es-M(es), es-oaxioms(es), es_val(es), es_info(es), es-pred?(es), es-eq(es), es-Msg(es), es-sends(es; l; e), es-Msgl(es; l), es-E(es), event_system{i:l}, f(a), kindcase(k; a.f(a); l,t.g(l;t)), x.A(x), idlnk-deq |